In recent years, a software system penetrates a general society, and reliability required for software becomes very high, while software has gotten more complex and bigger, and thus it is very difficult to secure quality by review in a manual work or a test.
A model checking technique as a method disclosed in for example, Non-patent Literature 1, is a technique that writes a behavior of software with an input language of a predetermined model checker and executes the predetermined model checker to comprehensively inspect a state which the software may take such as whether a property required for the software is satisfied. According to the method disclosed in Non-patent Literature 1, a functional property which the software needs to satisfy is inspected by writing a behavior of software with an input language called Promela and inputting the written behavior in a model checker called SPIN.
Further, according to a method disclosed in Non-patent Literature 6, a behavior of software and a time constraint are expressed as a timed automaton and input into a model checker called UPPAAL to inspect a process time which the software needs to satisfy.
The model checking technique is a technique which is promising to secure quality of software which has gotten more complex and bigger, but comprehensively inspects the state which software may take, and thus a phenomenon called a state explosion in which the number of states to be inspected is enormous occurs, and both or any one of a phenomenon, in which a time calculation amount required for processing becomes a realistically unallowable size, and a phenomenon, in which a space calculation amount required for processing exceeds a storage region mounted on a computer used in processing, occur, in large-scale software, and as a result, the inspection may not be completed.
In order to cope with the state explosion, processing called abstraction is performed with respect to a source code or an inspection code, and as a result, the number of states may be reduced to an inspectable range. The abstraction includes simplification of a branching condition of, for example, a selection statement. Since an execution path which was not present originally may be generated or an execution path which is present may be extinct by the abstraction, a property of software expressed by an inspected result for the inspection code may be different from an original software property. Therefore, it is preferable to examine a level of the abstraction by considering a property to be inspected with respect to software and then apply the abstraction.
Further, the model inspection technique may have a practical problem in that an effort to write software to be inspected with an input language of a predetermined model checker is large. In the method disclosed in Patent Literature 1, the source code is converted into the inspection code written in an input language of a predetermined model checker by using a translation map. The inspection code is inspected by the predetermined model checker by using an environment model defined by a user apart from the conversion. In addition, according to the method disclosed in Patent Literature 2, the source code is converted into an intermediate expression, and a parameter to satisfy a real-time constraint is generated to generate a timed automaton added with the parameter.
FIG. 15 illustrates one example of a model checking technique using a computer in the related art. In a model checking system in the related art, first, a design is modeled and thereafter, a timed automaton which conforms to an execution environment is prepared and automatic inspection is performed. By the automatic inspection, comprehensive performance validation for software to be inspected is achieved.
Further, as one of software development technologies, model-driven development is used. The model driven development is a technology of performing software development by describing design information of software as a model and refining the model by a converting operation. For example, in the model driven development, a format or a meaning of a model is defined by a meta model written in an MOF which is a method disclosed in Non-patent Literature 2, a conversion rule of refining a model is written in a QVT which is a method disclosed in Non-patent Literature 3, description and validation by a constraint associated with consistency or soundness by a model are performed by an OCL which is a method disclosed in Non-patent Literature 4, and a source code is generated from a model by a MOFM2T which is a method disclosed in Non-patent Literature 5.
Further, a “model” in the model checking technique and a “model” in the model driven development are concepts that are independent from each other, and there is generally no commonality associated with a data structure or a meaning.